package base;

import resolution.Resolution;

/**
 * Created by IntelliJ IDEA. User: njussien Date: 30/11/12 Time: 10:37
 */
public class Et extends OperateurBinaire {

	// ///////////////
	// CONSTRUCTOR //
	// ///////////////

	public Et(Formule a, Formule b) {
		super(a, b);
	}

	// ///////////
	// METHODS //
	// ///////////

	@Override
	public Formule negation() {
		return new Ou(this.operande.negation(), this.operandedroit.negation());
	}

	@Override
	public Formule descendreNon() {
		return new Et(operande.descendreNon(), operandedroit.descendreNon());
	}

	public String toString() {
		return "[Operande:(" + operande.toString() + " ET " + operandedroit.toString() + ")] ";
	}

	@Override
	public Formule enleveEquImp() {
		return new Et(operande.enleveEquImp(), operandedroit.enleveEquImp());
	}

	public void renommer() {

		Formule f = operande;
		int nbChang = 0;
		while (f instanceof Quantification) {

			if (f instanceof Existe) {
				Variable aSubstituer = new Variable(((Existe) f).getX().nom + nbChang);

				nbChang++;
				Formule f2 = operande;
				while (f2 instanceof Quantification) {

					if (((Quantification) f2).getX().equals(((Existe) f).getX())) {
						Variable avant = ((Quantification) f2).getX();
						((Quantification) f2).setX(aSubstituer);
						((Quantification) f2).substituer(avant, aSubstituer);
					}

					f2 = ((PourTout) f2).getF();
				}
				f2.renommer();
			}
			f = ((Quantification) f).getF();
		}

		f = operandedroit;
		// int nbChang =0;
		while (f instanceof Quantification) {

			if (f instanceof Existe) {
				Variable aSubstituer = new Variable(((Existe) f).getX().nom + nbChang);

				nbChang++;
				Formule f2 = operandedroit;
				while (f2 instanceof Quantification) {

					if (((Quantification) f2).getX().equals(((Existe) f).getX())) {
						Variable avant = ((Quantification) f2).getX();
						((Quantification) f2).setX(aSubstituer);
						((Quantification) f2).substituer(avant, aSubstituer);
					}

					f2 = ((PourTout) f2).getF();
				}
				f2.renommer();
			}
			f = ((Quantification) f).getF();
		}

		operande.renommer();
		operandedroit.renommer();
	}

	@Override
	public Formule remonterQuantificateurs() {

		operande = operande.remonterQuantificateurs();
		operandedroit = operandedroit.remonterQuantificateurs();
		Formule f = operande;
		// on change selon les proprietes
		while (f instanceof Quantification) {
			if (f instanceof Existe) {
				Formule f2 = operandedroit;
				while (f2 instanceof Quantification) {
					if (((Quantification) f2).getX().getName().equals(((Existe) f).getX().getName())) {
						operande.substituer(new Variable("varRemont" + Resolution.CHANGEMENT_RENOMMAGE_REMONTER_QUANTIF++), ((Existe) f).getX());
						break;
					}
					f2 = ((Quantification) f2).getF();
				}
			}
			f = ((Quantification) f).getF();

		}

		if (operande instanceof Quantification) {
			if (operande instanceof Existe) {
				return new Existe(((Quantification) operande).x, new Et(((Quantification) operande).getF().remonterQuantificateurs(), operandedroit.remonterQuantificateurs())).remonterQuantificateurs();
			} else {

				Formule fdroit = operandedroit;
				Formule fdroitPrecedant = null;
				while (fdroit instanceof Quantification) {
					if (((Quantification) fdroit).x.getName().equals(((Quantification) operande).x.getName())) {

						// on est assure par avance que l'on est dans le bon cas
						if (fdroitPrecedant == null) {
							operandedroit = ((Quantification) fdroit).getF();
						} else {

							((Quantification) fdroitPrecedant).setF(((Quantification) fdroit).getF());
						}
						break;
					} else {
						fdroitPrecedant = fdroit;
						fdroit = ((Quantification) fdroit).getF();
					}
				}

				return new PourTout(((Quantification) operande).x, new Et(((Quantification) operande).getF().remonterQuantificateurs(), operandedroit.remonterQuantificateurs())).remonterQuantificateurs();
			}
		} else if (operandedroit instanceof Quantification) {
			if (operandedroit instanceof Existe) {
				return new Existe(((Quantification) operandedroit).x, new Et((Quantification) operande.remonterQuantificateurs(), ((Quantification) operandedroit).getF().remonterQuantificateurs())).remonterQuantificateurs();
			} else {

				System.out.println(this);
				Formule fdroit = operande;
				Formule fdroitPrecedant = null;
				while (fdroit instanceof Quantification) {

					if (((Quantification) fdroit).x.getName().equals(((Quantification) operandedroit).x.getName())) {

						// on est assure par l'avance que l'on est dans le bon
						// cas
						if (fdroitPrecedant == null) {
							operande = ((Quantification) fdroit).getF();
						} else {

							((Quantification) fdroitPrecedant).setF(((Quantification) fdroit).getF());
						}
						break;
					} else {
						fdroitPrecedant = fdroit;
						fdroit = ((Quantification) fdroit).getF();
					}
				}

				return new PourTout(((Quantification) operandedroit).x, new Et(operande.remonterQuantificateurs(), ((Quantification) operandedroit).getF().remonterQuantificateurs())).remonterQuantificateurs();
			}
		} else {
			return this;
		}
	}

	@Override
	public Formule toConjonctive() {
		return new Et(operande.toConjonctive(), operandedroit.toConjonctive());
	}

	@Override
	public Formule copy() {
		return new Et(operande.copy(), operandedroit.copy());
	}

}
